{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.Finitary.Lift where

import GHC.TypeNats
import Data.Finite (Finite)
import Data.Functor.Classes (Eq1)
import Data.Kind (Type)

class (Eq1 f) => Finitary1 (f :: Type -> Type) where
  type LiftCardinality f (n :: Nat) :: Nat 
  liftFromFinite :: (KnownNat n) => (Finite n -> a) -> Finite (LiftCardinality f n) -> f a
  liftToFinite :: (KnownNat n) => (a -> Finite n) -> f a -> Finite (LiftCardinality f n)  
